#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"

int foo(int a, int b) {
	int c=klee_change(a,b);
	for (int i=0;i<klee_change(3,2);++i)
		c-=klee_change(b,a);
	
	return c;
}

int main(int argc, char *argv[]) {
  return foo(klee_change(5,900),klee_change(900,5));
}
